Commentary by Chris Pressey =========================== This work is distributed under a CC-BY-ND-4.0 license, with the following explicit exception: the ratings may be freely used for any purpose with no limitations. Lambda Calculus --------------- ### The Calculi of Lambda-Conversion * rating: classic . ### Introduction to Combinators and the Lambda Calculus * rating: TODO Barendregt 1984 should be on this list but isn't. So, this is. ### A Short Introduction to the Lambda Calculus * rating: 2 A fixed-point combinator can be given (the Y combinator), but in the simply-typed lambda calculus, it cannot be given a type. Thus recursion cannot be done in the STLC and thus the STLC is not Turing-complete. ### Introduction to Lambda Calculus * rating: 2 This is where I found out about Combinatory Reduction Systems from. ### Chapter 5: The Untyped Lambda Calculus * rating: 2 . ### Untyped Lambda Calculus * rating: 1 . ### A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure * rating: 1 So one thing I haven't wrapped my head around here, is that this lambda calculus has abstractions that take a list of parameters, instead of one abstraction each; which is a lot more like a conventional programming language (with functions but no currying by default). And this is isomorphic to the sequent calculus? Does this mean anything? ### The Lambda Calculus is Algebraic * rating: 3 "Yes, but what IS an indeterminate?" ### A Lambda Calculus with Naive Substitution * rating: 0 This paper is cited in something else I read -- possibly "Equational Logic as a Programming Language". I have read this paper, although maybe I missed the point when I did. Basically, the substitution operator substitutes using a list of positions, rather than a name? This seems underwhelming. ### A Graph-like Lambda Calculus for which Leftmost-Outermost Reduction is Optimal * rating: 1 I read this, but not entirely comprehendingly -- I could stand to read it again. This paper is cited in "Equational Logic as a Programming Language". Staples gives top-level rules for beta-reduction of the lambda calculus (after it has been converted to de Bruijn indexes) which are essentially algebraic-looking, and which resemble the S, K, I combinators: (\x.x G) -> G (\x.y G) -> y (where y =/= x) (\x.(E F) G) -> ((\x.E G) (\x.F G)) (\x.\y.E G) -> (\y.(\x E G)) Which seems to imply that you can derive the S, K, I combinators from analyzing the lambda calculus algebraically. Which seems weird, because I thought the S, K, I combinators came originally from (Schoenfinkel) taking that basic axiom system of Hilbert's and making them "point-free". But weirder things have happened. So, OK. ### On the Relation between the λμ-Calculus and the Syntactic Theory of Sequential Control * rating: TODO For a long time it has been widely thought that a classical proof, as opposed to an intuitionistic one, did not carry any computational content... but! Types-as-propositions. I guess by "Syntactic Theory of Sequential Control" they refer to continuations. ### functional programming - Is Lambda Calculus purely syntactic? - Computer Science Stack Exchange * rating: 1 . ### What are the axioms, inference rules, and (formal) semantics of lambda calculus? - Computer Science Stack Exchange * rating: 1 . ### lo.logic - What\'s the point of \$\\eta\$-conversion in lambda calculus? - Theoretical Computer Science Stack Exchange * rating: 1 . ### lambda calculus - What\'s the definition of equational theory? Why is λ logic free? - Mathematics Stack Exchange * rating: 1 . ### lo.logic - Scott on the consistency of the lambda calculus - MathOverflow * rating: 1 . ### Lambda Terms * rating: TODO . ### The largest number representable in 64 bits * rating: 1 . ### lo.logic - What\'t the smallest lambda calculus term which is not known to have a normal form? - MathOverflow * rating: 1 . ### maciej-bendkowski/lambda-sampler: Boltzmann sampler utilities for lambda calculus * rating: 1 .